Nuprl Definition : nat_op
13,42
postcript
pdf
n
x(
op
;
id
)
e
==
(
op
,
id
) 0
i
<
n
.
e
latex
Up
groups
1
Wellformedness Lemmas
nat
op
wf
Definitions
(
op
,
id
)
lb
i
<
ub
.
E
(
i
)
origin
(op,id) 0 
i < n. e (op,id) 0 i < n. e (op,id) lb i < ub. E(i)